comment |circumscription of a disjunction|

DECLARE INDVAR x;
DECLARE INDCONST a b;
DECLARE PREDCONST isblock 1;
DECLARE PREDPAR P 1;

AXIOM whichblock:	isblock(a)∨isblock(b);;

CIRCUMSCRIBE newaxiom isblock P x IN whichblock;

∧I newaxiom[P←λx.(x=a)];